es:ES, e':E, P:({e:E| loc(e) = loc(e')  Id }Prop). ee'.P(e)  P(e')  e<e'.P(e) 

latex

Definitions	P  Q, P & Q, P  Q, P  Q, ee'.P(e), P  Q, e<e'.P(e), x. t(x), x(s), Id, loc(e), Prop, E, x:A. B(x), t  T, ES, e  e' , x:A. B(x), A & B, (e <loc e'), T, True, 1of(t), SQType(T), {T}, first(e), A, False, b
Lemmas	es-le-loc, es-le wf, es-le-self, es-first wf, assert wf, not wf, es-loc-pred, true wf, squash wf, es-locl-iff, es-locl wf, event system wf, es-E wf, es-loc wf, Id wf, existse-before wf, existse-le wf